/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30



␈↓ α∧␈↓CS206␈↓ ¬$SOLUTIONS TO FINAL␈↓ 
lFALL 1976 

␈↓ α∧␈↓1. ␈↓↓noccurl[x , u] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ [␈↓αif␈↓↓ x = ␈↓αa␈↓↓ u ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ 0] + noccurl[x , ␈↓αd␈↓↓ u]␈↓.

␈↓ α∧␈↓2. ␈↓↓noccurs[x , y] ← ␈↓αif␈↓↓ x = y ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ y ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ noccurs[x , ␈↓αa␈↓↓ y] + noccurs[x, ␈↓αd␈↓↓ y]␈↓.

␈↓ α∧␈↓3.␈αThere␈α
are␈αmany␈αsolutions␈α
to␈αthe␈α␈↓↓samefringe␈↓␈α
problem␈αwhich␈αhas␈α
been␈αproposed␈αas␈α
an␈αexample
␈↓ α∧␈↓requiring co-routines.  Here one of the simplest:

␈↓ α∧␈↓␈↓↓samefringe[x, y] ← x ␈↓αeq ␈↓↓y ∨ [¬␈↓αat ␈↓↓x ∧ ¬␈↓αat ␈↓↓y ∧ same[gopher x, gopher y]]

␈↓ α∧␈↓↓same[x, y] ← ␈↓αa ␈↓↓x ␈↓αeq a y ∧ ␈↓↓samefringe[␈↓αd ␈↓↓ x, ␈↓αd ␈↓↓y]

␈↓ α∧␈↓↓gopher u ← ␈↓αif at a ␈↓↓u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ gopher ␈↓αaa ␈↓↓u . [␈↓αda ␈↓↓u . ␈↓αd ␈↓↓u] ␈↓

␈↓ α∧␈↓␈↓↓gopher␈↓␈α
digs␈α
up␈αthe␈α
first␈α
atom␈α
in␈αan␈α
S-expression,␈α
piling␈α
up␈αthe␈α
␈↓↓cdr␈↓s␈α
(with␈α
its␈αhind␈α
legs)␈α
so␈αthat␈α
the
␈↓ α∧␈↓indexing through the atoms can be continued.

␈↓ α∧␈↓4. ␈↓↓prinb[e, l] ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ e ␈↓αthen␈↓↓ e . l
␈↓ α∧␈↓↓␈↓ βd␈↓αelse␈↓↓ ␈↓LP␈↓↓ .
␈↓ α∧␈↓↓␈↓ ∧4[␈↓αif␈↓↓ ␈↓αn␈↓↓ ␈↓αd␈↓↓ e ␈↓αthen␈↓↓ prinb[␈↓αa␈↓↓ e, ␈↓RP␈↓↓ . l]
␈↓ α∧␈↓↓␈↓ ¬∧␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αd␈↓↓ e ␈↓αthen␈↓↓ prinb[␈↓αa␈↓↓ e, ␈↓DOT␈↓↓ . [␈↓αd␈↓↓ e . [␈↓RP␈↓↓ . l]]]
␈↓ α∧␈↓↓␈↓ ¬∧␈↓αelse␈↓↓ prinb[␈↓αa␈↓↓ e, ␈↓αd␈↓↓ prinb[␈↓αd␈↓↓ e, l]]]␈↓


␈↓ α∧␈↓5. Let ␈↓↓P(u)␈↓ be the assertion ␈↓↓drop[u * v] = drop u * drop v␈↓.  The induction principle is

␈↓ α∧␈↓␈↓ αT␈↓↓P[␈↓NIL␈↓↓] ∧ ∀u.[P[␈↓αd␈↓↓ u] ⊃ P[u]] ⊃ ∀u.P[u]␈↓,

␈↓ α∧␈↓and putting ␈↓↓P = λu.[drop[u * v] = drop u * drop v]␈↓ gives

␈↓ α∧␈↓␈↓ β∀␈↓↓[drop[␈↓NIL␈↓↓ * v] = drop ␈↓NIL␈↓↓ * drop v]
␈↓ α∧␈↓↓␈↓ βd∧ ∀u.[drop[␈↓αd␈↓↓ u * v] = drop ␈↓αd␈↓↓ u * drop v ⊃ drop[u * v] = drop u * drop v]

␈↓ α∧␈↓↓␈↓ β∀⊃ ∀u.[drop[u * v] = drop u * drop v]␈↓.

␈↓ α∧␈↓We have

␈↓ α∧␈↓␈↓↓drop[␈↓NIL␈↓↓ * v]␈↓ βd= drop v␈↓ εt␈↓by ␈↓↓∀w.␈↓NIL␈↓↓ * w = w,

␈↓ α∧␈↓↓␈↓ βd= ␈↓NIL␈↓↓ * drop v␈↓ εt␈↓by same fact,

␈↓ α∧␈↓␈↓ βd= drop NIL * drop v␈↓ εtdrop NIL = NIL comes from def. of ␈↓↓drop␈↓,

␈↓ α∧␈↓and the last equation is ␈↓↓P[␈↓NIL␈↓↓]␈↓.  The induction step is




␈↓ α∧␈↓␈↓ ε|1␈↓ ∧



␈↓ α∧␈↓␈↓↓drop[u * v]␈↓ β4= drop[␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u .[q u * v]]␈↓ 
↑␈↓by def. ␈↓↓u * v

␈↓ α∧␈↓↓␈↓ β4= ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ drop v ␈↓αelse␈↓↓ drop[␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]␈↓ 
.␈↓by distrib. of c.e.␈↓↓

␈↓ α∧␈↓↓␈↓ β4= ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ drop v ␈↓αelse␈↓↓ <␈↓αa␈↓↓ [␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]> . drop ␈↓αd␈↓↓ [␈↓αa␈↓↓ u .[␈↓αd␈↓↓ u * v]]
␈↓ α∧␈↓↓␈↓by def. of ␈↓↓drop␈↓ and ␈↓↓∀x y.¬␈↓αn␈↓↓[x . y]␈↓,

␈↓ α∧␈↓␈↓ β4= ␈↓αif␈↓ ␈↓αn␈↓ u ␈↓αthen␈↓ drop v ␈↓αelse␈↓ <␈↓αa␈↓ u> . drop [␈↓αd␈↓ u * v]␈↓ 
*by ␈↓αa␈↓ and ␈↓αd␈↓ rules,␈↓↓

␈↓ α∧␈↓↓␈↓ β4= ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ drop v ␈↓αelse␈↓↓ <␈↓αa␈↓↓ u> . [drop ␈↓αd␈↓↓ u * drop v]␈↓ 	?␈↓by induction hypothesis␈↓↓,

␈↓ α∧␈↓↓␈↓ β4= ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ * drop v ␈↓αelse␈↓↓ [<␈↓αa␈↓↓ u> . drop ␈↓αd␈↓↓ u] * drop v
␈↓ α∧␈↓↓␈↓by ␈↓↓∀w.[␈↓NIL␈↓↓ * w = w]␈↓ and def. of ␈↓↓[<␈↓αa␈↓↓ u> . drop ␈↓αd␈↓↓ u] * drop v,

␈↓ α∧␈↓↓␈↓ β4= [␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ <␈↓αa␈↓↓ u> . drop ␈↓αd␈↓↓ u] * drop v␈↓ 
]␈↓distrib. of c.e␈↓↓

␈↓ α∧␈↓↓␈↓ β4= drop u * drop v␈↓␈↓ 
&by def. of ␈↓↓drop v␈↓,

␈↓ α∧␈↓which is the result to be proved.

␈↓ α∧␈↓6. ␈↓↓compact x ← ␈↓αa␈↓↓ compact1[x, ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓compact1[x, u] ←␈↓ βt{find[x, u]}[λz.
␈↓ α∧␈↓↓␈↓ ∧4␈↓αif␈↓↓ ¬␈↓αn␈↓↓ z ␈↓αthen␈↓↓ ␈↓αa␈↓↓ z . u
␈↓ α∧␈↓↓␈↓ ∧4␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x . u
␈↓ α∧␈↓↓␈↓ ∧4␈↓αelse␈↓↓ {compact1[␈↓αa␈↓↓ x, u]}[λx1.
␈↓ α∧␈↓↓␈↓ ¬∧{compact1[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ x1]}[λx2.
␈↓ α∧␈↓↓␈↓ ¬T␈↓αif␈↓↓ ␈↓αa␈↓↓ x ␈↓αeq␈↓↓ ␈↓αa␈↓↓ x1 ∧ ␈↓αd␈↓↓ x ␈↓αeq␈↓↓ ␈↓αa␈↓↓ x2 ␈↓αthen␈↓↓ x . [x . ␈↓αd␈↓↓ x2]
␈↓ α∧␈↓↓␈↓ ¬T␈↓αelse␈↓↓ {␈↓αa␈↓↓ x1 . ␈↓αa␈↓↓ x2}[λv. v . [v . ␈↓αd␈↓↓ x2]]]]]

␈↓ α∧␈↓↓find[x, u] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αa␈↓↓ u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ find[x, ␈↓αd␈↓↓ u]

␈↓ α∧␈↓␈↓ αTThe␈αfollowing␈αsolution␈αby␈α
Roy␈αHarrington␈αseems␈αbetter␈αthan␈α
mine,␈αbut␈αI␈αhaven't␈αtaken␈α
time
␈↓ α∧␈↓to analyze it:

␈↓ α∧␈↓␈↓↓compact x ← comp[x, ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓comp[x, y] ←␈↓ βD␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x
␈↓ α∧␈↓↓␈↓ βD␈↓αelse␈↓↓ {mem[x,y]}[λs.␈↓ ¬T␈↓αif␈↓↓ ¬␈↓αn␈↓↓ s ␈↓αthen␈↓↓ s
␈↓ α∧␈↓↓␈↓ ¬T␈↓αelse␈↓↓ {comp[␈↓αd␈↓↓ x, y]}[λz. comp[␈↓αa␈↓↓ x, z . y] . z]]

␈↓ α∧␈↓↓mem[x, y] ←␈↓ β4␈↓αif␈↓↓ x = y ␈↓αthen␈↓↓ y
␈↓ α∧␈↓↓␈↓ β4␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ y ␈↓αthen␈↓↓ ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ β4␈↓αelse␈↓↓ {mem[x, ␈↓αa␈↓↓ y]}[λz. ␈↓αif␈↓↓ ␈↓αn␈↓↓ z ␈↓αthen␈↓↓ mem[x, ␈↓αd␈↓↓ y] ␈↓αelse␈↓↓ z]]





␈↓ α∧␈↓␈↓ ε|2␈↓ ∧